A,B:es_realizer{i:l}.
(Rplus?(A))
 (i:Id. fpf-compatible(Knd; k.Type; Kind-deq; R-da(Rplus-left(A); i); R-da(Rplus-right(A); i)))
 (R-interface(B; A)  (R-interface(B; Rplus-left(A))  R-interface(B; Rplus-right(A)))) 

latex

Definitions

T, True, prop{i:l}, top, fpf-cap(f; eq; x; z), P  Q, if b then t else f fi , tt, ff, x. t(x), t  T, P  Q, R-interface(A; B), P  Q, Rplus-right(x1), Rplus-left(x1), R-da(R; i), Rplus?(x1), b, P  Q, x:A. B(x), fpf-compatible(A; a.B(a); eq; f; g), , False, x(s), Unit, es_realizer{i:l}, Rrframe(loc; x; L), Rbframe(loc; k; L), Raframe(loc; k; L), Rpre(loc; ds; a; p; P), Rsends(ds; knd; T; l; dt; g), Reffect(loc; ds; knd; T; x; f), Rsframe(lnk; tag; L), Rframe(loc; T; x; L), Rinit(loc; T; x; v), Rplus(left; right), Rnone,

Lemmas

true wf, squash wf, subtype rel wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, not wf, bnot wf, assert wf, fpf-ap wf, lsrc wf, fpf-dom wf, rcv wf, top wf, fpf-trivial-subtype-top, ldst wf, R-da wf, Kind-deq wf, fpf-join-cap-sq, fpf-join wf, fpf-cap wf, es realizer wf, false wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf